Nuprl Lemma : Rinit-discrete_wf 11,40

A:es_realizer{i:l}. (Rinit?(A))  (Rinit-discrete(A 
latex


DefinitionsRinit-discrete(A), t  T, P  Q, x:AB(x), prop{i:l}
Lemmases realizer wf, Rinit? wf, assert wf, bfalse wf, btrue wf, Rinit-v wf

origin